A:Type, B:(AType), eq:EqDecider(A), x:A, y:B(x), a:Atom1.
AtomFree(Type;A)
 AtomFree(AType;B)
 (x:A. AtomFree(A;x))
 AtomFree(EqDecider(A);eq)
 y:B(x)>>a
 <x,y>:x:AB(x)>>a 

latex

Definitions	Prop, t  T, x:T>>a, P  Q, x(s), x:A. B(x), x:A. B(x), P  Q, P & Q, P  Q, true, x. t(x), false, if b t else f fi, 2of(t), 1of(t), Unit, , {T}, SQType(T),
Lemmas	deq wf, atom-free wf, inheres wf, matters wf, assert wf, bfalse wf, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, deq property, pi2 wf, eqtt to assert, bool wf, pi1 wf, eqof wf, bool sq